Inference at * 1 2 
Iof proof for Lemma integer sqrt:

.....upcase..... NILNIL

1. n : 
2. 0 < n
3. r:. (((r * r)  (n - 1)) & ((n - 1) < ((r+1) * (r+1))))
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by D (-1) THEN Auto 

latex

 1: 

 1: 3. r : 
 1: 4. (r * r)  (n - 1)
 1: 5. (n - 1) < ((r+1) * (r+1))
 1:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 .

Definitions	#$n, {x:A| B(x)} , , A  B, A, False, P  Q, x:A. B(x), P & Q, x:A  B(x), x:AB(x), Void, a < b, , n - m, -n, n+m, n * m
Lemmas	nat wf